$\forall$$T$, $A$:Type, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow$$A$$\rightarrow$Prop), $f$:(State(${\it ds}$)$\rightarrow$$A$$\rightarrow$$T$).
\\[0ex]Normal($A$)
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}$). Dec($\exists$$v$:$A$. $P$($s$,$v$)))
\\[0ex]$\Rightarrow$ at src($l$):action a(m) precondition $P$ sends [tg,$f$] on link $l$ $\in$ Realizer